Nuprl Lemma : proper-at-join
0,22
postcript
pdf
A
,
B
:MsgA. Feasible(
A
)
Feasible(
B
)
(
A
||+
B
)
Feasible(
A
B
)
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
MsgA
,
Feasible(
M
)
,
A
||+
B
,
M1
M2
Lemmas
ma-compat
wf
,
ma-feasible
wf
,
msga
wf
,
ma-join-feasible
origin
A, B:MsgA. Feasible(A) 
Feasible(B) (A ||+ B) Feasible(A 
B) A, B:MsgA. Feasible(A) Feasible(B) (A ||+ B) Feasible(A B) 
T Qx:A. B(x) M2